Nuprl Lemma : R-sub-Rlist
0,22
postcript
pdf
L
:Realizer List,
A
:Realizer. (
A
L
)
A
(
L
)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
P
Q
,
(
L
)
,
reduce(
f
;
k
;
as
)
,
Y
,
P
Q
,
P
Q
,
P
Q
,
Prop
,
x
.
t
(
x
)
,
P
&
Q
,
(
x
l
)
,
x
:
A
.
B
(
x
)
,
A
&
B
,
||
as
||
,
x
(
s
)
,
{
T
}
Lemmas
es
realizer
wf
,
l
member
wf
,
all
functionality
wrt
iff
,
R-sub
wf
,
Rplus
wf
,
Rlist
wf
,
implies
functionality
wrt
iff
,
cons
member
,
R-sub-plus-left
,
R-sub-lemma1
origin
L:Realizer List, A:Realizer. (A 
L) 
A 
(L) L:Realizer List, A:Realizer. (A L) A (L) x:A. B(x) T Q(L)
Q
Q Q
x. t(x) l)
x:A. B(x)